자연 연역

자연 연역은 논리 체계의 종류 중 하나로, 도입과 소거 규칙을 통해 정의되는 특징을 가지고 있다. 게르하르트 겐첸이 그의 1935년 논문 (Gentzen 1935a, 1935b, 1969)에서 시퀀트 계산과 함께 발표하였다.

도입과 소거 규칙

도입 규칙 (introduction rule)은 개별 명제들에 대한 판단으로부터 이들로 구성된 복합적인 명제에 대한 판단을 이끌어 내는 추론 규칙이다. 반대로 소거 규칙 (elimination rule)은 복합적인 명제에 대한 판단에서 이를 구성하는 개별 명제에 대한 판단을 이끌어 낸다.

연언

연언은 한개의 도입 규칙 \(\wedge I\)와 두개의 소거 규칙 \(\wedge E_1, \wedge E_2\)를 가진다. \[ \begin{prooftree} \AxiomC{ $\phi$ } \AxiomC{ $\psi$ } \RightLabel{ $\wedge I$ } \BinaryInfC{ $\phi \wedge \psi$ } \end{prooftree} \quad \begin{prooftree} \AxiomC{ $\phi \wedge \psi$ } \RightLabel{ $\wedge E_1$ } \UnaryInfC{ $\phi$ } \end{prooftree} \quad \begin{prooftree} \AxiomC{ $\phi \wedge \psi$ } \RightLabel{ $\wedge E_2$ } \UnaryInfC{ $\psi$ } \end{prooftree} \]

선언

선언은 두개의 도입 규칙 \(\vee I_1, \vee I_2\)와 한개의 소거 규칙 \(\vee E\)를 가진다. \[ \newcommand{\Hyp}[2] {\AxiomC{}\RightLabel{#1}\UnaryInfC{#2}} \newcommand{\HypJ}[3] {\Hyp{#1}{#2}\noLine\UnaryInfC{$\vdots$}\noLine\UnaryInfC{#3}} \begin{prooftree} \AxiomC{ $\phi$ } \RightLabel{ $\vee I_1$ } \UnaryInfC{ $\phi \vee \psi$ } \end{prooftree} \quad \begin{prooftree} \AxiomC{ $\psi$ } \RightLabel{ $\vee I_2$ } \UnaryInfC{ $\phi \vee \psi$ } \end{prooftree} \quad \begin{prooftree} \AxiomC{ $\phi \vee \psi$ } \HypJ{$u$}{$\phi$}{$\chi$} \HypJ{$v$}{$\psi$}{$\chi$} \RightLabel{ $\vee E^{u,v}$ } \TrinaryInfC{ $\chi$ } \end{prooftree} \]

함언

함언은 도입 규칙 \(\to\! I\)와 소거 규칙 \(\to\! E\)를 가진다. \[ \begin{prooftree} \HypJ{$u$}{$\phi$}{$\psi$} \RightLabel{ $\to\! I^u$ } \UnaryInfC{ $\phi \to \psi$ } \end{prooftree} \quad\quad\qquad \begin{prooftree} \AxiomC{ $\phi \to \psi$ } \AxiomC{ $\phi$ } \RightLabel{ $\to\! E$ } \BinaryInfC{ $\psi$ } \end{prooftree} \]

참 연결사

참 연결사는 도입 규칙 \(\top I\)를 가지며 소거 규칙이 존재하지 않는다. \[ \begin{prooftree} \AxiomC{ } \RightLabel{ $\top I$ } \UnaryInfC{ $\top$ } \end{prooftree} \]

거짓 연결사

거짓 연결사는 도입 규칙이 존재하지 않으며 소거 규칙 \(\bot E\)를 가진다. \[ \begin{prooftree} \AxiomC{ $\bot$ } \RightLabel{ $\bot E$ } \UnaryInfC{ $\chi$ } \end{prooftree} \]

부정

부정은 도입 규칙 \(\neg I\)와 소거 규칙 \(\neg E\)를 가진다. \[ \begin{prooftree} \HypJ{$u$}{$\phi$}{$\bot$} \RightLabel{ $\neg I^u$ } \UnaryInfC{ $\neg \phi$ } \end{prooftree} \quad\quad\quad \begin{prooftree} \AxiomC{ $\neg \phi$ } \AxiomC{ $\phi$ } \RightLabel{ $\neg E$ } \BinaryInfC{ $\bot$ } \end{prooftree} \]

부정 \(\neg \phi\)는 \(\phi \to \bot\)과 동치이기 때문에, 부정 연결사를 별도로 넣지 않는 경우도 있다.

보편 양화사

\[ \begin{prooftree} \AxiomC{ $\phi a$ } \RightLabel{ $\forall I$ } \UnaryInfC{ $\forall x. \phi x$ } \end{prooftree} \quad \begin{prooftree} \AxiomC{ $\forall x. \phi x$ } \RightLabel{ $\forall E$ } \UnaryInfC{ $\phi t$ } \end{prooftree} \] \(\forall I\) 규칙의 고유변수(eigenvariable) \(a\)는 \(\forall x. \phi x\)나 다른 가정에 나타나선 안된다.

존재 양화사

\[ \begin{prooftree} \AxiomC{ $\phi t$ } \RightLabel{ $\exists I$ } \UnaryInfC{ $\exists x. \phi x$ } \end{prooftree} \quad \begin{prooftree} \AxiomC{ $\exists x. \phi x$ } \HypJ{$u$}{$\phi a$}{$\chi$} \RightLabel{ $\exists E^u$ } \BinaryInfC{ $\chi$ } \end{prooftree} \] \(\exists E\) 규칙의 고유변수 \(a\)는 \(\exists x. \phi x\)와 \(\chi\), 다른 가정에 나타나선 안된다.

NJ

겐첸의 자연 연역 체계 NJ는 \(\wedge, \vee, \to, \bot, \neg, \forall, \exists\)로 구성된 직관주의적 1차 자연 연역 체계 이다.

예시

다음은 겐첸의 논문에서 제시된 NJ-증명의 예시이다. \[ \begin{prooftree} \Hyp{ $u$ }{ $P \vee (Q \wedge R)$ } \Hyp{ $v$ }{ $P$ } \RightLabel{ $\vee I_1$ } \UnaryInfC{ $P \vee Q$ } \Hyp{ $v$ }{ $P$ } \RightLabel{ $\vee I_1$ } \UnaryInfC{ $P \vee R$ } \RightLabel{ $\wedge I$ } \BinaryInfC{ $(P \vee Q) \wedge (P \vee R)$ } \Hyp{ $w$ }{ $Q \wedge R$ } \RightLabel{ $\wedge E_1$ } \UnaryInfC{ $Q$ } \RightLabel{ $\vee I_2$ } \UnaryInfC{ $P \vee Q$ } \Hyp{ $w$ }{ $Q \wedge R$ } \RightLabel{ $\wedge E_2$ } \UnaryInfC{ $R$ } \RightLabel{ $\vee I_2$ } \UnaryInfC{ $P \vee R$ } \RightLabel{ $\wedge I$ } \BinaryInfC{ $(P\vee Q)\wedge(P\vee R)$ } \RightLabel{ $\vee E^{v,w}$ } \TrinaryInfC{ $(P\vee Q)\wedge(P\vee R)$ } \RightLabel{ $\to\! I^u$ } \UnaryInfC{ $P \vee (Q \wedge R) \to (P\vee Q)\wedge(P\vee R)$ } \end{prooftree} \]

\[ \begin{prooftree} \Hyp{$u$}{$\exists x. \forall y. Fxy$} \Hyp{$v$}{$\forall y. Fay$} \RL{$\forall E$} \UIC{$Fab$} \RL{$\exists I$} \UIC{$\exists x. Fxb$} \RL{$\forall I$} \UIC{$\forall y. \exists x. Fxy$} \RL{$\exists E^v$} \BIC{$\forall y. \exists x. Fxy$} \RL{$\to\! I^u$} \UIC{$(\exists x. \forall y. Fxy) \to (\forall y. \exists x. Fxy)$} \end{prooftree} \]

\[ \begin{prooftree} \Hyp{$u$}{$\neg \exists x. Fx$} \Hyp{$v$}{$Fa$} \RL{$\exists I$} \UIC{$\exists x. Fx$} \RL{$\neg E$} \BIC{$\bot$} \RL{$\neg I^v$} \UIC{$\neg Fa$} \RL{$\forall I$} \UIC{$\forall y. \neg Fy$} \RL{$\to\! I^u$} \UIC{$(\neg \exists x. Fx) \to (\forall y. \neg Fy)$} \end{prooftree} \]

NK

겐첸은 NJ에 배중률을 추가한 고전적 자연 연역 체계 NK를 제시하였다. 즉 다음과 같은 공리꼴을 도입한다. \[ \phi \vee \neg \phi \]

고전적 체계를 얻기 위해, 배중률과 동치인 이중 부정 소거(double negation elimination)를 추론 규칙으로 추가하는 방법도 있다. \[ \begin{prooftree} \AxiomC{ $\neg\neg\phi$ } \RightLabel{ $\neg\neg E$ } \UnaryInfC{ $\phi$ } \end{prooftree} \]

그러나 이중 부정 소거 규칙은 부정의 도입 규칙으로부터 정당화 되지 않음에 주의하여야 한다. 겐첸은 이에 대해 다음과 같이 언급했다(Gentzen 1935a, 1935b, 1969).

However, such a schema still falls outside the framework of the NJ-inference figures, because it represents a new elimination of the negation whose admissibility does not follow at all from our method of introducing the ¬-symbol by the ¬-I.